;; The first four lines of this file were added by Dracula.
;; They tell DrScheme that this is a Dracula Modular ACL2 program.
;; Leave these lines unchanged so that DrScheme can properly load this file.
#reader(planet "reader.rkt" ("cce" "dracula.plt") "modular" "lang")
(require "mresize.lisp")
(require "mbmptree.lisp")
(require "mavltree.lisp")
(require "mdatagenerators.lisp")

(module Tresize
  (import Iresize)
  (import Ibmptree)
  (import Iavltree)
  (import IDataGenerators)
  
  (include-book "testing" :dir :teachpacks)
  (include-book "doublecheck" :dir :teachpacks)
  
  ; Generates a random pixel (random RGB values).
  (defrandom random-pixel ()
    (let* ((r (random-between 0 255))
           (g (random-between 0 255))
           (b (random-between 0 255)))
      (list r g b)))
  
  ; Random bitmap file, uses a static header with a 
  ; size of heightxwidth.
  (defrandom random-bitmap (height width)
    (let* ((header (list 66 77 54 12 0 0 0 0 0 0 54 0 0 
                         0 40 0 0 0 width 0 0 0 height 0 0 0 1 
                         0 24 0 0 0 0 0 0 12 0 0 0 0 0 
                         0 0 0 0 0 0 0 0 0 0 0 0 0))
           (pixels (random-list-of (random-pixel) :size (* width height)))
           (tr (insert-header (empty-bmp-tree) header)))
      (fill-bitmap tr 0 0 height width pixels)))

  ; Creates a 4x4 bmp-tree for testing
  (defun test-tree-4x4 ()
    (make-bmp-tree
     (list (list 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 4 0 0 0 4)
           (list 0 0 (list 45 166 97)) (list 0 1 (list 83 211 244))
           (list 0 2 (list 200 100 50)) (list 0 3 (list 122 11 99))
           (list 1 0 (list 73 21 255)) (list 1 1 (list 3 144 196))
           (list 1 2 (list 14 155 250)) (list 1 3 (list 111 88 2))
           (list 2 0 (list 101 66 37)) (list 2 1 (list 91 226 199))
           (list 2 2 (list 5 17 30)) (list 2 3 (list 25 1 235))
           (list 3 0 (list 51 177 136)) (list 3 1 (list 15 49 34))
           (list 3 2 (list 0 4 10)) (list 3 3 (list 253 239 216)))))
  
  (defun test-tree-6x4 ()
    (make-bmp-tree
     (list (list 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 4 0 0 0 6)
           (list 0 0 (list 45 166 97)) (list 0 1 (list 83 211 244))
           (list 0 2 (list 200 100 50)) (list 0 3 (list 122 11 99))
           (list 1 0 (list 73 21 255)) (list 1 1 (list 3 144 196))
           (list 1 2 (list 14 155 250)) (list 1 3 (list 111 88 2))
           (list 2 0 (list 101 66 37)) (list 2 1 (list 91 226 199))
           (list 2 2 (list 5 17 30)) (list 2 3 (list 25 1 235))
           (list 3 0 (list 51 177 136)) (list 3 1 (list 15 49 34))
           (list 3 2 (list 0 4 10)) (list 3 3 (list 253 239 216))
           (list 4 0 (list 51 177 136)) (list 4 1 (list 15 49 34))
           (list 4 2 (list 0 4 10)) (list 4 3 (list 253 239 216))
           (list 5 0 (list 51 177 136)) (list 5 1 (list 15 49 34))
           (list 5 2 (list 0 4 10)) (list 5 3 (list 253 239 216)))))

  (defun test-tree-4x6 ()
    (make-bmp-tree
     (list (list 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 6 0 0 0 4)
           (list 0 0 (list 45 166 97)) (list 0 1 (list 83 211 244))
           (list 0 2 (list 200 100 50)) (list 0 3 (list 122 11 99))
           (list 0 4 (list 200 100 50)) (list 0 5 (list 122 11 99))
           (list 1 0 (list 73 21 255)) (list 1 1 (list 3 144 196))
           (list 1 2 (list 14 155 250)) (list 1 3 (list 111 88 2))
           (list 1 4 (list 200 100 50)) (list 1 5 (list 122 11 99))
           (list 2 0 (list 101 66 37)) (list 2 1 (list 91 226 199))
           (list 2 2 (list 5 17 30)) (list 2 3 (list 25 1 235))
           (list 2 4 (list 200 100 50)) (list 2 5 (list 122 11 99))
           (list 3 0 (list 51 177 136)) (list 3 1 (list 15 49 34))
           (list 3 2 (list 0 4 10)) (list 3 3 (list 253 239 216))
           (list 3 4 (list 200 100 50)) (list 3 5 (list 122 11 99)))))
     
  (defun test-tree-4x7 ()
    (make-bmp-tree
     (list (list 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 6 0 0 0 4)
           (list 0 0 (list 45 166 97)) (list 0 1 (list 83 211 244))
           (list 0 2 (list 200 100 50)) (list 0 3 (list 122 11 99))
           (list 0 4 (list 200 100 50)) (list 0 5 (list 122 11 99))
           (list 0 6 (list 123 213 32))
           (list 1 0 (list 73 21 255)) (list 1 1 (list 3 144 196))
           (list 1 2 (list 14 155 250)) (list 1 3 (list 111 88 2))
           (list 1 4 (list 200 100 50)) (list 1 5 (list 122 11 99))
           (list 1 6 (list 123 213 32))
           (list 2 0 (list 101 66 37)) (list 2 1 (list 91 226 199))
           (list 2 2 (list 5 17 30)) (list 2 3 (list 25 1 235))
           (list 2 4 (list 200 100 50)) (list 2 5 (list 122 11 99))
           (list 2 6 (list 123 213 32))
           (list 3 0 (list 51 177 136)) (list 3 1 (list 15 49 34))
           (list 3 2 (list 0 4 10)) (list 3 3 (list 253 239 216))
           (list 3 4 (list 200 100 50)) (list 3 5 (list 122 11 99))
           (list 3 6 (list 123 213 32)))))

  (defun test-tree-7x4 ()
    (make-bmp-tree
     (list (list 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 4 0 0 0 7)
           (list 0 0 (list 45 166 97)) (list 0 1 (list 83 211 244))
           (list 0 2 (list 200 100 50)) (list 0 3 (list 122 11 99))
           (list 1 0 (list 73 21 255)) (list 1 1 (list 3 144 196))
           (list 1 2 (list 14 155 250)) (list 1 3 (list 111 88 2))
           (list 2 0 (list 101 66 37)) (list 2 1 (list 91 226 199))
           (list 2 2 (list 5 17 30)) (list 2 3 (list 25 1 235))
           (list 3 0 (list 51 177 136)) (list 3 1 (list 15 49 34))
           (list 3 2 (list 0 4 10)) (list 3 3 (list 253 239 216))
           (list 4 0 (list 51 177 136)) (list 4 1 (list 15 49 34))
           (list 4 2 (list 0 4 10)) (list 4 3 (list 253 239 216))
           (list 5 0 (list 51 177 136)) (list 5 1 (list 15 49 34))
           (list 5 2 (list 0 4 10)) (list 5 3 (list 253 239 216))
           (list 6 0 (list 51 177 136)) (list 6 1 (list 15 49 34))
           (list 6 2 (list 0 4 10)) (list 6 3 (list 253 239 216)))))
           
  ; Tests with legal input
  (check-expect (get-dimensions (resize (test-tree-4x4) 250)) 
                (cons 10 10))
  (check-expect (get-dimensions (resize (test-tree-6x4) 250)) 
                (cons 15 10))
  (check-expect (get-dimensions (resize (test-tree-4x6) 250)) 
                (cons 10 15))
  ; Since the new width would be 17.5 pixels, it is truncated to
  ; 17 pixels. In order to maintain the aspect ratio of the new
  ; bitmap as much as possible, the old height is multiplied by
  ; the ratio of the old width to the new width and then truncated
  ; which results in a new height of 9 which is less than the 
  ; expected value of 10. This is a result of the resize algorithm
  ; we used.
  (check-expect (get-dimensions (resize (test-tree-4x7) 250)) 
                (cons 9 17))
  ; Since the algorithm bases its resize ratio off of the width,
  ; the same is not true if the height is rounded down. In this 
  ; case, the new width still has the expected value of 10. 
  (check-expect (get-dimensions (resize (test-tree-7x4) 250)) 
                (cons 17 10))
  
  ; nil test
  (check-expect (get-dimensions (resize nil 250)) nil)
  ; Tests with illegal input
  (check-expect (bmp-tree? (resize (list (list 0 0 (list 3 3 3)) 
                                         (list 0 1 (list 5 5 5))
                                         (list 1 0 (list 7 7 7))
                                         (list 1 1 (list 9 9 9))) 
                                   150)) nil)
  (check-expect (bmp-tree? 
                 (resize (avl-insert nil 1 (list 0 (list 5 5 5)))
                         50)) nil)
  (check-expect (resize (test-tree-4x4) 155.5) (test-tree-4x4))
  
  ; Verifies that the resize function always returns a true bmp-tree
  (defproperty resize-returns-true-bmp-tree-prp
    (height :value (random-between 5 25)
     width :value (random-between 5 25)
     perc :value (random-between 20 200)
     bitmap :value (random-bitmap height width))
    (true-bmp-tree? (resize bitmap perc)))

  ; Verifies that the resize function always returns a bitmap with 
  ; the correct size
  (defproperty resize-returns-correct-dimensions-prp
    (height :value (random-between 5 25)
     width :value (random-between 5 25)
     perc :value (random-between 20 200)
     bitmap :value (random-bitmap height width))
    (let* ((newbmp (resize bitmap perc))
           (oldDim (get-dimensions bitmap))
           (oldHt (car oldDim))
           (oldWd (cdr oldDim))
           (newDim (get-dimensions newbmp))
           (newHt (car newDim))
           (newWd (cdr newDim)))
      (and (equal newWd (truncate (* oldWd (/ perc 100)) 1))
           ; due to the algorithm used, the new height is equal
           ; to the old height multiplied by the ratio of the new
           ; width to the old width rather than the old height
           ; multiplied by the percentage ratio
           (equal newHt 
                  (truncate (* oldHt (/ newWd oldWd)) 1)))))
            
  ; Round trip property definition for resize
  (defproperty resize-200-50-round-trip-prp
    (height :value (random-between 5 15)
     width :value (random-between 5 15)
     bitmap :value (random-bitmap height width))
    (equal bitmap
           (resize (resize bitmap 200) 50)))
  )

(link RTresize (Mavltree Mbmptree Mdatagenerators Mresize Tresize))
(invoke RTresize)
  